star-append(T;P;Q)(L)
== LL:(T List) List, L':T List. (XLL. P(X)) & Q(L') & L = (concat(LL) @ L') 

latex

---

clarification:

star-append(T;P;Q)(L)
== LL:(T List) List, L':T List.
== l_all(LL;T List;X.P(X)) & Q(L') & L = (concat(LL) @ L')  T List 

latex

Definitions	star-append(T;P;Q), x:A. B(x), xL. P(x), P & Q, as @ bs, concat(ll)
FDL editor aliases	star-append